theory Peterson imports Main Clang
begin

datatype procnames = ProcP | ProcQ

datatype shnames = InterP | InterQ | Turn

datatype lbs = lint | ltur | lcs | lreset

text {*
Process ProcP: shared (InterP: bool; InterQ: bool; Turn: bool)
\\{
\\   while true do
\\ lint: InterP := true;
\\ ltur: Turn := false; /* "Q" */
\\     wait InterQ = false | Turn = true /* "P" */ do
\\ lcs:   /* critical section */
\\     end;
\\ lreset: InterP := false;
\\   end
\\}
*}

--"program term"
definition psrc where
"psrc = (Proc (Phdr ProcP [] [(Vdecl InterP BoolT), (Vdecl InterQ BoolT), (Vdecl Turn BoolT)])
  (Cwhile None (Bex (Eimm (BoolV True))) 
     (Cseq None 
    (Cwrite (Some lint) InterP (Eimm (BoolV True))) 
     (Cseq None 
    (Cwrite (Some ltur) Turn (Eimm (BoolV False))) 
     (Cseq None 
    (Cwait None ([Weq InterQ (Eimm (BoolV False)), Weq Turn (Eimm (BoolV True))]) 
      (Cnone (Some lcs))
    ) 
    (Cwrite (Some lreset) InterP (Eimm (BoolV False))) 
     )))
  )
)"

text {*
Process ProcQ: shared (InterP: bool; InterQ: bool; Turn: bool)
\\{
\\   while true do
\\ lint: InterQ := true;
\\ ltur: Turn := true; /* "P" */
\\     wait InterP = false | Turn = false /* "Q" */ do
\\ lcs:   /* critical section */
\\     end;
\\ lreset: InterQ := false;
\\   end
\\}
*}

--"program term"
definition qsrc where
"qsrc = (Proc (Phdr ProcQ [] [(Vdecl InterP BoolT), (Vdecl InterQ BoolT), (Vdecl Turn BoolT)])
  (Cwhile None (Bex (Eimm (BoolV True))) 
     (Cseq None 
    (Cwrite (Some lint) InterQ (Eimm (BoolV True))) 
     (Cseq None 
    (Cwrite (Some ltur) Turn (Eimm (BoolV True))) 
     (Cseq None 
    (Cwait None ([Weq InterP (Eimm (BoolV False)), Weq Turn (Eimm (BoolV False))]) 
      (Cnone (Some lcs))
    )  
    (Cwrite (Some lreset) InterQ (Eimm (BoolV False))) 
    )))
  )
)"

definition petalg where "petalg \<equiv> [psrc, qsrc]"

(*------------------------------------------------------------------------------------------------------------------*)

--"Program petalg is well-formed"
theorem wf_petalg: "wf_prog petalg" 
  by (simp only: petalg_def, normalization)

end
